package ch.epfl.lara.matcheck.util;

import ch.epfl.lara.matcheck.ast._



object FreshTree extends Environment with ShapeKeeper {
  
  def apply(tree: Tree): Tree = fresh(tree).setPos(tree.pos)
    
    
  
  private def fresh[T<:Tree](tree: T): T = (tree match {
    case Program(constr,extr,objs,klasses) => 
      cast[T,Program]  (Program(constr,extr,objs.map(fresh(_)),klasses.map(fresh(_))))
    
    case ClassDef(isSealed,isAbs,name,fields,superc,inv,methods) =>
      cast[T,ClassDef] (ClassDef(isSealed,isAbs,name,fields,superc,inv,methods.map(fresh(_))))
          
    case ObjectDef(name,inv,methods) =>
      cast[T,ObjectDef] (ObjectDef(name,inv,methods.map(fresh(_))))
      
    case MethodDef(name,params,tpe,ppc,body) =>
      var local_map = empty_map
      val fresh_params_name = params.map(p => FreshName.fresh(p.getName)) //methodParams(params.size)
      val fresh_params = for(i<-List.range(0,fresh_params_name.length)) yield {
        val ParamDef(pname,tpe) = params(i)
        local_map = local_map.update(pname.getName,fresh_params_name(i))
        ParamDef(new Name[VarSymbol](fresh_params_name(i),pname.getSym),tpe)
      }
    
      val fresh_ppc = ppc match {
        case None => None
        case Some((pre,post)) => 
          Some((Substitute(local_map,pre),Substitute(local_map,post)))
      }
      cast[T,MethodDef]  (MethodDef(name,fresh_params,tpe,fresh_ppc,fresh(Substitute(local_map,body))))
    
    case e : Expr => cast[T,Expr] (fresh(empty_map,e))
    
    case _ => error(this+": Don't know what to do with ") 
  }).setPos(tree.pos)
  
  
  private def fresh[T<:Expr](env: Env, expr: T): T = {
    def iter[T<:Expr](expr: T): T = (expr match {
      case ObjectId(name)         => expr
      case Ident(name)            => expr
      case True  | Number(_) |  
           False | StringLit(_)   => expr
      case Call(obj,method,args)  => cast[T,Call]          (Call(iter(obj),method,args.map(iter(_))))
      case Select(obj,field)      => cast[T,Select]        (Select(iter(obj),field))
      case If(cond,then,elze)     => cast[T,If]            (If(iter(cond),iter(then),iter(elze)))
      case New(name,args)         => cast[T,New]           (New(name,args.map(iter(_))))
      case IsInstanceOf(expr,tpe) => cast[T,IsInstanceOf]  (IsInstanceOf(iter(expr),tpe))
      case +(left,right)          => cast[T,+]             (new +(iter(left),iter(right)))
      case -(left,right)          => cast[T,-]             (new -(iter(left),iter(right)))
      case *(left,right)          => cast[T,*]             (new *(iter(left),iter(right)))
      case /(left,right)          => cast[T,/]             (new /(iter(left),iter(right)))
      case %(left,right)          => cast[T,%]             (new %(iter(left),iter(right)))
      case ==(left,right)         => cast[T,==]            (new ==(iter(left),iter(right)))
      case <(left,right)          => cast[T,<]             (new <(iter(left),iter(right)))
      case <=(left,right)         => cast[T,<=]            (new <=(iter(left),iter(right)))
      case &&(left,right)         => cast[T,&&]            (new &&(iter(left),iter(right)))
      case ||(left,right)         => cast[T,||]            (new ||(iter(left),iter(right)))
      case !(f)                   => cast[T,!]             (new !(iter(f)))
      case ->(left,right)         => cast[T,->]            (new ->(iter(left),iter(right)))
      case Match(scrut,tpe,cases) => cast[T,Match]         (new Match(iter(scrut),tpe,cases.map(fresh(env,_))))
    }).setPos(expr.pos)
    
    iter(expr)
  }
  
  
  
  private def fresh(env: Env, kase: CaseDef ): CaseDef = {
    def bindings(p: PatternDef): List[(String,String)] = p match {
      case Wildcard                    => Nil
      case VarPattern(name,tpe)        => List((name.getName,FreshName.fresh(name.getName)))
      case ClassPattern(objname,args)  => args.flatMap(bindings(_))
    }
    
    val CaseDef(pos,pattern,guard,body) = kase
  
    val new_bindings    = bindings(pattern)
    val new_context     = env ++ (new_bindings) 
    val updated_pattern = Substitute(new_context,pattern)
    val updated_guard   = guard match { 
                            case Some(g) => Some(cast[Expr,Expr] (Substitute(new_context,g))) 
                            case None    => guard
                          }
    val updated_body    = cast[Expr,Expr]  (Substitute(new_context,body))
    CaseDef(pos,updated_pattern,updated_guard,fresh(new_context,updated_body)).setPos(kase.pos)
  }
  
  
  override def toString = "FreshTree"
  
 
}




